$\vdash$  $\forall$$T$:Type, $L$:($T$ List). ($\exists$$x$:$T$. ($x$ $\in$ $L$)) $\Leftarrow\!\Rightarrow$ (0 $<$ $\parallel$$L$$\parallel$)